/*
 * RepeatedLiteralsRemover.cuh
 *
 *  Created on: Oct 10, 2013
 *      Author: jaime
 */

#ifndef REPEATEDLITERALSREMOVER_CUH_
#define REPEATEDLITERALSREMOVER_CUH_

#include "../SATSolver/SolverTypes.cuh"
#include <stdlib.h>
#include <vector>

using namespace std;

class RepeatedLiteralsRemover {
private:
	vector<Clause> * formula;
	int number_of_variables;
	sat_status status;

	// Auxiliary attributes
	sat_status* stats;

	/**
	 * Process clause, removing repeated literals.
	 * Return true if the clause must be removed, false otherwise.
	 */
	bool process_clause(Clause & clause);

public:
	RepeatedLiteralsRemover(vector<Clause> & formula, int number_of_variables);
	~RepeatedLiteralsRemover();

	void process();
	sat_status get_status();

};

#endif /* REPEATEDLITERALSREMOVER_CUH_ */
